active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
F(mark(X)) → F(X)
PROPER(g(X)) → PROPER(X)
ACTIVE(f(f(a))) → G(f(a))
TOP(mark(X)) → PROPER(X)
ACTIVE(f(X)) → ACTIVE(X)
ACTIVE(f(X)) → F(active(X))
TOP(ok(X)) → ACTIVE(X)
ACTIVE(f(f(a))) → F(g(f(a)))
PROPER(f(X)) → F(proper(X))
F(ok(X)) → F(X)
TOP(mark(X)) → TOP(proper(X))
PROPER(g(X)) → G(proper(X))
G(ok(X)) → G(X)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(mark(X)) → F(X)
PROPER(g(X)) → PROPER(X)
ACTIVE(f(f(a))) → G(f(a))
TOP(mark(X)) → PROPER(X)
ACTIVE(f(X)) → ACTIVE(X)
ACTIVE(f(X)) → F(active(X))
TOP(ok(X)) → ACTIVE(X)
ACTIVE(f(f(a))) → F(g(f(a)))
PROPER(f(X)) → F(proper(X))
F(ok(X)) → F(X)
TOP(mark(X)) → TOP(proper(X))
PROPER(g(X)) → G(proper(X))
G(ok(X)) → G(X)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
G(ok(X)) → G(X)
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(ok(X)) → G(X)
The value of delta used in the strict ordering is 1/16.
POL(ok(x1)) = 1/4 + (2)x_1
POL(G(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
F(mark(X)) → F(X)
F(ok(X)) → F(X)
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X)) → F(X)
F(ok(X)) → F(X)
The value of delta used in the strict ordering is 4.
POL(mark(x1)) = 1 + x_1
POL(ok(x1)) = 4 + (4)x_1
POL(F(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
The value of delta used in the strict ordering is 4.
POL(PROPER(x1)) = (4)x_1
POL(f(x1)) = 4 + (4)x_1
POL(g(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ACTIVE(f(X)) → ACTIVE(X)
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(f(X)) → ACTIVE(X)
The value of delta used in the strict ordering is 1/16.
POL(f(x1)) = 1/4 + (2)x_1
POL(ACTIVE(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(mark(X)) → TOP(proper(X))
Used ordering: Polynomial interpretation [25,35]:
TOP(ok(X)) → TOP(active(X))
The value of delta used in the strict ordering is 1/16.
POL(active(x1)) = (2)x_1
POL(f(x1)) = x_1
POL(a) = 1/4
POL(g(x1)) = (1/4)x_1
POL(mark(x1)) = 1/4 + (4)x_1
POL(ok(x1)) = (4)x_1
POL(TOP(x1)) = (1/4)x_1
POL(proper(x1)) = (4)x_1
active(f(X)) → f(active(X))
active(f(f(a))) → mark(f(g(f(a))))
proper(f(X)) → f(proper(X))
f(mark(X)) → mark(f(X))
proper(g(X)) → g(proper(X))
proper(a) → ok(a)
g(ok(X)) → ok(g(X))
f(ok(X)) → ok(f(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
TOP(ok(X)) → TOP(active(X))
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(ok(X)) → TOP(active(X))
The value of delta used in the strict ordering is 2.
POL(active(x1)) = (4)x_1
POL(f(x1)) = x_1
POL(a) = 2
POL(g(x1)) = 1/2
POL(ok(x1)) = 1 + (4)x_1
POL(mark(x1)) = 1/4 + (2)x_1
POL(TOP(x1)) = (2)x_1
active(f(X)) → f(active(X))
active(f(f(a))) → mark(f(g(f(a))))
f(mark(X)) → mark(f(X))
f(ok(X)) → ok(f(X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
active(f(f(a))) → mark(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))